\begin{tabbing}
$\forall$$T$:Type. 
\\[0ex]($\forall$$x$,$y$:$T$. decidable(($x$ = $y$)))
\\[0ex]$\Rightarrow$ \=($\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$), $x$:Id.\+
\\[0ex]es{-}dtype(${\it es}$; loc($e$); $x$; $T$)
\\[0ex]$\Rightarrow$ \=($\forall$${\it e'}$$\leq$$e$.es{-}when(${\it es}$; $x$; ${\it e'}$) = es{-}when(${\it es}$; $x$; $e$) $\in$ $T$\+
\\[0ex]$\vee$ \=$\exists$${\it e'}$$<$$e$.@${\it e'}$($x$$\rightarrow$es{-}when(${\it es}$; $x$; $e$))\+
\\[0ex]$\wedge$ $\forall$${\it e''}$$\in$(${\it e'}$,$e$].es{-}when(${\it es}$; $x$; ${\it e''}$) = es{-}when(${\it es}$; $x$; $e$) $\in$ $T$))
\-\-\-
\end{tabbing}